A:Type, f:a:A fp Type, eq:EqDecider(A), x:A, z:Type. f(x)?z  Type 

latex

Definitions	EqDecider(T), f(x)?z, Unit, P  Q, P & Q, x  dom(f), a:A fp B(a), Top, f(x), x. t(x), P  Q, , Prop, b, A, b, x:A. B(x), t  T
Lemmas	assert wf, not wf, bnot wf, fpf-ap wf, bool wf, fpf-trivial-subtype-top, fpf-dom wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, fpf wf, deq wf